Search for: All records

A swarm of unmanned aerial vehicles (UAVs) can be used for many applications, including disaster relief, search and rescue, and establishing communication networks, due to its mobility, scalability, and robustness to failure. However, a UAV swarm’s performance is typically limited by each agent’s stored energy. Recent works have considered the usage of thermals, or vertical updrafts of warm air, to address this issue. One challenge lies in a swarm of UAVs detecting and taking advantage of these thermals. Inspired by hawks, a swarm could take advantage of thermals better than individuals due to the swarm’s distributed sensing abilities. To determine which emergent behaviors increase survival time, simulation software was created to test the behavioral models of UAV gliders around thermals. For simplicity and robustness, agents operate with limited information about other agents. The UAVs’ motion was implemented as a Boids model, replicating the behavior of flocking birds through cohesion, separation, and alignment forces. Agents equipped with a modified behavioral model exhibit dynamic flocking behavior, including relative ascension-based cohesion and relative height-based separation and alignment. The simulation results show the agents flocking to thermals and improving swarm survival. These findings present a promising method to extend the flight time of autonomous UAV swarms. 

Most software domains rely on compilers to translate high-level code to multiple different machine languages, with performance not too much worse than what developers would have the patience to write directly in assembly language. However, cryptography has been an exception, where many performance-critical routines have been written directly in assembly (sometimes through metaprogramming layers). Some past work has shown how to do formal verification of that assembly, and other work has shown how to generate C code automatically along with formal proof, but with consequent performance penalties vs. the best- known assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce, with mechanized proof (in Coq) whose final theorem statement mentions little beyond the input functional program and the operational semantics of x86-64 assembly. On the optimization side, we apply randomized search through the space of assembly programs, with repeated automatic benchmarking on target CPUs. On the formal-verification side, we connect to the Fiat Cryptography framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker, incorporating a modest subset of known features of SMT solvers and symbolic-execution engines. The overall prototype is quite practical, e.g. producing new fastest-known implementations of finite-field arithmetic for both Curve25519 (part of the TLS standard) and the Bitcoin elliptic curve secp256k1 for the Intel 12𝑡ℎ and 13𝑡ℎ generations.